In this thesis I present a tool to automatically generate TLA+ refinement mappings. These mappings are used in the Inverse Implementation Method developed by Lau [Lau11]. The Inverse Implementation Method is a process for software validation. It is integrated into the development process of Java software with a TLA+ specification.

At the beginning of the thesis I give an introduction to the Inverse Implementation Method. I therefore cover the process of the validation and the critical parts that are involved. Then I explain the general idea of refinement mappings and their application in the Inverse Implementation Method, where they pose as a bond between implementation and specification. Thereafter I analyse an example mapping and present the five different kinds of mappings included. Lastly I give a conclusion in which I highlight the advantages of the automatically generated mappings, describe their limitations and encourage further work.

The main contribution of my thesis and the tool I developed is that it makes the Inverse Implementation Method easier to use. The automated generation of the critical refinement mappings enables even programmers not familiar with the method to validate their code. They don’t need specific knowledge about the internal parts of the validation process because the generated mappings abstracts form that.

The idea for this thesis originated in a bachelor course about formal specification with TLA+ and a talk of Lau about his work on the Inverse Implementation Method. Parts of this thesis have already been presented at the Formal Methods 2012 TLA+ Workshop in Paris (France) [FM212].